(set-logic QF_BV)
(set-option :model_validate true)
(set-option :sat.local_search true)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const v17 Bool)
(declare-const bv_20-0 (_ BitVec 20))
(declare-const v18 Bool)
(assert (and v16 v5 v17 v4 v1 v15 v16 v9 v18))
(declare-const v20 Bool)
(push 1)
(declare-const v24 Bool)
(assert (= v14 v9 (=> v18 v24) (and v5 v7 v4 v7 (and v16 v5 v17 v4 v1 v15 v16 v9 v18) v0 v2 v8 v20) (and v7 (distinct v16 v11 v17 v6 v7 v2 v14 v16 v5) v18 v1 v14 v10 v4)))
;(push 1)
(check-sat)